/*
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.util.ints;

import java.util.NoSuchElementException;

/**
 * An implementation of the IntTreeSet interface based on a balanced binary
 * search tree.
 *
 * @specfield ints: set int
 * @author Emina Torlak
 */
public final class IntTreeSet extends AbstractIntSet implements Cloneable {

    /*
     * The endpoints of the ranges in the tree do not touch, and they are sorted by
     * their right endpoints.
     * @invariant all n: tree.nodes | n.max = n.key && n.min <= n.max && all n':
     * tree.nodes - n | n'.max < n.min - 1 || n'.min > n.max + 1
     */
    private final IntTree<Range> tree;
    private int                  size;

    /**
     * Constructs an empty int set.
     *
     * @ensures no this.ints'
     */
    public IntTreeSet() {
        tree = new IntTree<Range>();
        size = 0;
    }

    /**
     * Constructs a new int set containing the elements in the specified set.
     *
     * @ensures this.ints' = s.ints
     * @throws NullPointerException s = null
     */
    public IntTreeSet(IntSet s) {
        this();
        addAll(s);
    }

    /**
     * Copy constructor.
     *
     * @ensures constructs a deep copy of the original set.
     */
    private IntTreeSet(IntTreeSet original) {
        this.size = original.size;
        try {
            this.tree = original.tree.clone();
        } catch (CloneNotSupportedException e) {
            throw new InternalError(); // unreachable code
        }
    }

    // public String toString() {
    // for(Range next = tree.min(); next != null; next = tree.successor(next) )
    // {
    // System.out.print("[" + next.min + " .. " + next.key+ "] ");
    // }
    // System.out.println("");
    // return "";
    // }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.util.ints.IntSet#iterator(int,int)
     */
    @Override
    public IntIterator iterator(int from, int to) {
        return from <= to ? new AscendingIterator(from, to) : new DescendingIterator(from, to);
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.util.ints.IntSet#size()
     */
    @Override
    public int size() {
        return size;
    }

    /**
     * Returns true if i is in this set.
     *
     * @return i in this.ints
     * @see kodkod.util.ints.IntSet#contains(int)
     */
    @Override
    public boolean contains(int i) {
        final Range r = tree.searchGTE(i);
        return r != null && r.min <= i;
    }

    /**
     * Returns the smallest element in this set. Throws a NoSuchElementException if
     * this set is empty.
     *
     * @return min(this.ints)
     * @throws java.util.NoSuchElementException no this.ints
     * @see kodkod.util.ints.IntSet#min()
     */
    @Override
    public int min() {
        checkNonEmpty();
        return tree.min().min;
    }

    /**
     * Returns the largest element in this set. Throws a NoSuchElementException if
     * this set is empty.
     *
     * @return max(this.ints)
     * @throws java.util.NoSuchElementException no this.ints
     * @see kodkod.util.ints.IntSet#max()
     */
    @Override
    public int max() {
        checkNonEmpty();
        return tree.max().key;
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.util.ints.IntSet#floor(int)
     */
    @Override
    public int floor(int i) {
        checkNonEmpty();
        Range r = tree.searchGTE(i);
        if (r == null || r.min > i) {
            r = tree.searchLTE(i);
            return r == null ? null : r.key;
        } else
            return i;
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.util.ints.IntSet#ceil(int)
     */
    @Override
    public int ceil(int i) {
        checkNonEmpty();
        final Range r = tree.searchGTE(i);
        return r == null ? null : StrictMath.max(i, r.min);
    }

    /**
     * Adds the given integer to this set if not already present and returns true.
     * Otherwise does nothing and returns false.
     *
     * @ensures this.ints' = this.ints + i
     * @return i in this.ints'
     * @see kodkod.util.ints.IntSet#add(int)
     */
    @Override
    public boolean add(int i) {
        final Range ceil = tree.searchGTE(i);
        if (ceil == null || ceil.min > i) {

            final Range floor = tree.searchLTE(i);

            if (floor != null && floor.key == i - 1) {
                if (ceil != null && ceil.min == i + 1) {
                    tree.delete(ceil);
                    floor.key = ceil.key;
                } else {
                    floor.key = i;
                }
            } else if (ceil != null && ceil.min == i + 1) {
                ceil.min = i;
            } else {
                tree.insert(new Range(i, i));
            }

            size++;
            return true;
        }

        return false;
    }

    /**
     * Removes the given integer from this set if already present and returns true.
     * Otherwise does nothing and returns false.
     *
     * @ensures this.ints' = this.ints - i
     * @return i !in this.ints'
     * @see kodkod.util.ints.IntSet#remove(int)
     */
    @Override
    public boolean remove(int i) {
        final Range ceil = tree.searchGTE(i);

        if (ceil != null && i >= ceil.min) {
            if (ceil.min == ceil.key) {
                tree.delete(ceil);
            } else if (i == ceil.min) {
                ceil.min++;
            } else if (i == ceil.key) {
                ceil.key = i - 1;
            } else { // split the range in two
                tree.insert(new Range(ceil.min, i - 1));
                ceil.min = i + 1;
            }
            size--;
            assert size >= 0;
            return true;
        }

        return false;
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.util.ints.IntSet#containsAll(kodkod.util.ints.IntCollection)
     */
    @Override
    public boolean containsAll(IntCollection other) {
        if (other instanceof IntTreeSet) {
            IntTreeSet s = (IntTreeSet) other;
            if (size >= s.size) {
                for (Range r1 = s.tree.min(); r1 != null; r1 = s.tree.successor(r1)) {
                    Range r0 = tree.searchGTE(r1.key);
                    if (r0 == null || r1.min < r0.min)
                        return false;
                }
                return true;
            }
            return false;
        }
        return super.containsAll(other);
    }

    /**
     * Removes all elements from this set.
     *
     * @ensures no this.ints'
     * @see kodkod.util.ints.IntCollection#clear()
     */
    @Override
    public void clear() {
        tree.clear();
        size = 0;
    }

    /**
     * Returns a copy of this int tree set. The copy is independent of this IntSet.
     *
     * @return a copy of this IntSet.
     * @see kodkod.util.ints.IntSet#clone()
     */
    @Override
    public IntTreeSet clone() {
        // ok to use copy constructor to clone a final class
        return new IntTreeSet(this);
    }

    /**
     * A range of integers in an int set.
     *
     * @specfield min: int
     * @specfield max: int
     * @invariant min <= max
     * @invariant max = key
     * @author Emina Torlak
     */
    private static final class Range extends IntTree.Node<Range> implements Cloneable {

        private int min;

        Range(int min, int max) {
            super(max);
            this.min = min;
        }

        @Override
        protected Range clone() throws CloneNotSupportedException {
            return (Range) super.clone();
        }

    }

    /**
     * An iterator that traverses the ints in this set in the ascending order.
     *
     * @author Emina Torlak
     */
    private final class AscendingIterator implements IntIterator {

        private Range     next;
        private final int endpoint;
        private int       currentMax, cursor, lastReturned;
        private boolean   canRemove;

        /**
         * @requires from <= to
         */
        AscendingIterator(int from, int to) {
            endpoint = to;
            lastReturned = Integer.MIN_VALUE;
            canRemove = false;
            next = tree.searchGTE(from);
            if (next == null) {
                cursor = 0;
                currentMax = -1;
            } else {
                cursor = StrictMath.max(next.min, from);
                currentMax = next.key;
                next = tree.successor(next);
            }
        }

        @Override
        public boolean hasNext() {
            if (cursor > currentMax) {
                if (next == null)
                    return false;
                this.cursor = next.min;
                this.currentMax = next.key;
                next = tree.successor(next);
            }
            return lastReturned < Integer.MAX_VALUE && cursor <= endpoint;
        }

        @Override
        public int next() {
            if (!hasNext())
                throw new NoSuchElementException();
            canRemove = true;
            return lastReturned = cursor++;
        }

        @Override
        public void remove() {
            if (!canRemove)
                throw new IllegalStateException();
            IntTreeSet.this.remove(lastReturned);
            next = tree.searchGTE(cursor);
            canRemove = false;
        }

    }

    /**
     * An iterator that traverses the ints in this set in the descending order.
     *
     * @author Emina Torlak
     */
    private final class DescendingIterator implements IntIterator {

        private Range     next;
        private final int endpoint;
        private int       currentMin, cursor, lastReturned;
        private boolean   canRemove;

        /**
         * @requires from >= to
         */
        DescendingIterator(int from, int to) {
            endpoint = to;
            lastReturned = Integer.MAX_VALUE;
            canRemove = false;
            next = tree.searchGTE(from);
            if (next == null || next.min > from) {
                next = tree.searchLTE(from);
                if (next == null) {
                    cursor = -1;
                    currentMin = 0;
                } else {
                    cursor = StrictMath.min(next.key, from);
                    currentMin = next.min;
                }
            } else {
                cursor = StrictMath.min(next.key, from);
                currentMin = next.min;
            }
        }

        @Override
        public boolean hasNext() {
            if (cursor < currentMin) {
                if (next == null)
                    return false;
                this.cursor = next.key;
                this.currentMin = next.min;
                next = tree.predecessor(next);
            }
            return lastReturned > Integer.MIN_VALUE && cursor >= endpoint;
        }

        @Override
        public int next() {
            if (!hasNext())
                throw new NoSuchElementException();
            canRemove = true;
            return lastReturned = cursor--;
        }

        @Override
        public void remove() {
            if (!canRemove)
                throw new IllegalStateException();
            IntTreeSet.this.remove(lastReturned);
            next = tree.searchLTE(cursor);
            canRemove = false;
        }

    }

}
